test_case1()
== case TERMOF{decidable q-constraints:ObjectId, 1:l}
== case (1
== case ,[<j.if j <z 2 then [1; 2][j] else 0 fi , 0>])
== of inl(y) => inl (y.1) 
== o| inr(x) => inr "not"  

latex

---

clarification:

test_case1()
== case TERMOF{decidable q-constraints:ObjectId, 1:l}
== case (1
== case ,[<j.if j <z 2 then [1 / [2 / []]][j] else 0 fi , 0> / []])
== of inl(y) => inl (y.1) 
== o| inr(x) => inr "not"  

latex

Definitions	case b of inl(x) => s(x) | inr(y) => t(y), f(a), decidable q-constraints, <a, b>, x.A(x), if b then t else f fi , i <z j, l[i], [car / cdr], #$n, [], inl x , t.1, inr x , "$token"
FDL editor aliases	test_case1